\section{Rozšírenia teórie}

V nasledujúcej časti budeme definovať rozšírenia,
ktoré v istom zmysle ani nepomôžu ani
neuberú sile teórii.

\begin{definicia}[Rozšírenie jazyka]
%%% {{{
    Jazyk $L'$ je rozšírením jazyka $L$, ak každý
    špeciálny symbol jazyka $L$ (prípadne aj symbol ``='')
    je v jazyku $L'$ obsiahnutý s rovnakým významom a s rovnakou árnosťou.
%%% }}}
\end{definicia}

\begin{priklad}
    Nech jazyk $L'$ je jazyk s rovnosťou a špeciálnymi symbolmi
    ``$<$'' a ``$0$''.
    Jazyk $L$ má symboly ``$<$'' a ``$=$''.
    Jazyk $L'$ je potom rozšírením jazyka $L$.
\end{priklad}    

\begin{definicia}[Rozšírenie teórie]
%%% {{{
    Majme teóriu $T'$ s jazykom $L'$. Hovoríme, že $T'$ je
    rozšírením teórie $T$ s jazykom $L$, ak platí,
    že $L'$ je rozšírením jazyka $L$ a pre každý formulu $A$ jazyku $L$
    platí $T \provable A \then T' \provable A$. 
%%% }}}    
\end{definicia}

\begin{priklad}
    Uvažujme teóriu grúp -- je to teória s rovnosťou, ktorá
    používa špeciálny symbol ``$+$'' a existuje v nej neutrálny prvok
    ``0''.
    
    Axiómy tejto teórie sú:
    \begin{itemize}
    \item $\forall x,y,z: (x+y)+z = x+(y+z)$
    \item $(x+0) = x = (0+x)$
    \item $(x+(-x)) = 0 = ((-x)+x)$
    \end{itemize}

    Ak si vezmeme relačnú štruktúru 
    $\mathcal{M}=\langle \mathbb{N}_0,0,+,- \rangle$,
    táto realizuje jazyk teórie grúp.
    Nie je však jej modelom (lebo nie všetky axiómy sú splnené, menovite
    napríklad inverzné prvky).
    Pokiaľ ale vezmeme $\mathcal{M}=\langle \mathbb{Z},0,+,- \rangle$,
    táto množina je realizáciou a zároveň aj modelom teórie grúp.  

    Teraz si zoberme jazyk $L = \{0,1,+,-,*, ^{-1}\}$
    a uvažujme postupne nasledujúce teórie:
    \begin{enumerate}
    \item teória grúp
    \item teória okruhov
    \item teória oborov integrity
    \item teória telies
    \item teória polí
    \item teória zväzov
    \end{enumerate}
    Každá z týchto teórii je rozšírením tej predchádzajúcej.
\end{priklad}

\begin{poznamka}
    Je dôležité si uvedomiť, že nie všetky axiómy pôvodnej teórie $T$
    sa musia nachádzať aj v rozšírenej teórii $T'$ -- 
    stačí, ak sa dajú odvodiť v $T'$.
\end{poznamka}

\begin{poznamka}
 Ak teória $T'$ nad jazykom $L'$ je rozšírením teórie $T$ nad jazykom
 $L$ a vieme že $T'$ je bezosporná, potom aj $T$ je bezosporná.
\end{poznamka}
\begin{dokaz}
    Predpokladajme, že $T$ je sporná teória. Teda je v nej dokázateľná
    každá formula.
    Špeciálne, je dokázateľné $T \provable A$ a $T \provable \neg A$.
    Keďže $T'$ je rozšírenie, musí potom platiť
    $T' \provable A$ a $T' \provable \neg A$. To je ale spor.
    \\
\end{dokaz}

\begin{definicia}[Konzervatívne rozšírenie]
    Hovoríme, že teória $T'$ nad jazykom $L'$ je konzervatívnym
    rozšírením teórie $T$ nad jazykom $L$, ak pre každú formulu
    $A$ nad jazykom $L$ platí $T' \provable A \then T \provable A$.
    Inak povedané, konzervatívnym rozšírením nezískame žiadne nové 
    teorémy.
\end{definicia}

\begin{poznamka}
    Spojením posledných dvoch definícii dostávame, že pre
    konzervatívne rozšírenie $T',L'$ teórie $T,L$ platí
    \begin{equation*}
        \forall A \in L:\quad\quad T \provable A \iff T' \provable A
    \end{equation*}
\end{poznamka}

\begin{poznamka}
    Nech $T',L'$ je konzervatívne rozšírenie $T,L$. Potom platí (z
    predchádzajúcej poznámky)
    $T$ je bezosporná $\iff$ $T'$ je bezosporná.
\end{poznamka}

\begin{veta}[Henkinova] 
    K ľubovoľnej teórii $T$ môžeme zostrojiť Henkinovu
    teóriu $T_H$, ktorá je konzervatívnym rozšírením teórie $T$.
\end{veta}    

\begin{dokaz}
%%% {{{
    Teóriu $T$ rozšírime a priradíme k nej teóriu $T_H$ tak, že
    jednak rozšírime jazyk teórie a jednak pridáme axiómy.
    Nech teória $T$ má jazyk $L$.
    Budeme tvoriť rozšírený jazyk $L_H$ tak, že budeme pridávať konštanty:

    Pre každú formulu $A$ napísanú v jazyku $L$,
    ktorá má jedinú {\it voľnú} premennú $x$ 
    vytvoríme konštanty $c_A, c_{\neg A}$
    a nasledovné axiomy: 
    \begin{itemize}
        \item[H1:]  $(\exists x) A \implies A_x[c_A]$
        \item[H2:]  $A_x[c_{\neg A}] \implies (\forall x) A$
    \end{itemize}

    Stačil by nám aj jeden typ axiómy, ako sa môžeme ľahko presvedčiť:
    \begin{itemize}
        \item $(\exists x) \neg A \implies \neg A_x[c_{\neg A}]$ -- H1
        \item $\neg \neg A_x[c_{\neg A}] \implies
                (\forall x) \neg \neg A$ -- obmena implikácie
        \item $A_x[c_{\neg A}] \implies (\forall x) A$ -- odstránenie
            dvojitej negácie
    \end{itemize}

    Konštanty $c_A, c_{\neg A}$ nazývame henkinovské konštanty prvého
    rádu. Tieto konštanty nám vytvoria množinu konštánt, označme ju
    $C_1$. Týmito konštantami rozšírime jazyk $L$.
    
    Teraz zoberme formulu $B$ na jazyku $L(C_1)$, ktorá obsahuje práve
    jednu voľnú premennú a aspoň jednu konštantu z $C_1$. K tejto
    formule priradíme podobne ako minule konštanty $c_B, c_{\neg B}$.
    Takto dosiahnuté konštanty budeme nazývať Henkinovské konštanty
    druhého rádu a ich množinu označíme ako $C_2$.
    
    Induktívne pokračujeme ďalej a podobne vytvárame množinu $C_3,
    C_4, \dots$
    Množinu $C_{n+1}$ vo všeobecnosti vytvoríme z množiny $C_n$, tak,
    že zoberieme formuly nad jazykom $L(C_n)$, ktoré obsahujú jednu
    voľnú premennú a aspoň jednu konštantu $n$-tého rádu.

    Označme si teraz
    \begin{equation*}
        L(C) = L \union \bigcup_{i=1}^{\infty} C_i
    \end{equation*}
    Teóriu $T_H$ bude tvoriť rozšírenie $L(C)$ jazyka $L$,
    axiómy budú axiómy $T$ ku ktorým pridáme všetky axiómy $H1$.
    Je ihneď zrejmé, že $T_H$ je rozšírenie teórie $T$.
    Potrebujeme ukázať, že $T_H$ je konzervatívne rozšírenie teórie $T$, t.j.
    že pre každú formulu $A$ jazyka $L$ platí 
    $T_H \provable A \Rightarrow T \provable A$.

    \medskip
    Poďme to dokázať:
    \begin{itemize}
    \item
        Nech platí, že v $T_H$ je dokázateľná formula $A$
        a nech $B_1, B_2, \dots, B_n$ sú všetky Henkinovské
        axiómy vyskytujúce sa v dôkaze $A$. Keďže dôkaz je konečný, týchto
        axióm je konečný počet. Ďalej môžeme uvažovať (ako sme už ukázali),
        že všetky axiómy $B_1, \ldots, B_n$ sú typu $H1$.
        Máme teda
        \begin{equation*}
            T, B_1, \dots ,B_n \provable A
        \end{equation*}

    \item
    Keďže axiómy $B_1,\ldots,B_n$ sú uzavreté formuly,
    môžeme použiť vetu o dedukcii a dostávame
    \begin{equation*}
        T \provable B_1 \implies B_2 \implies \ldots \implies B_n \implies A
    \end{equation*}

    \item
    Axiómy navyše môžeme poprehadzovať tak,
    aby $B_1$ obsahovala konštantu maximálneho rádu.
    Tvrdíme, že táto konštanta sa určite nenachádza v $A$ (pretože je
    nad pôvodným jazykom $L$)
    a ani v ostatných $B_i$
    (pretože všetky axiómy $B_i$ rovnakého rádu majú svoju
    ``hlavnú'' konštantu inú).
    Teda $B_1$ je tvaru $(\exists x) D \implies D_x[c_D]$,
    pričom $c_D$ nie je je použitá
    v $A,B_2,B_3, \ldots, B_n$. 
    \begin{equation*}
        T \provable \highlighta{((\exists x) D \implies D_x[c_D])} \implies 
            \highlightc{[B_2 \implies \ldots \implies B_n \implies A]}
    \end{equation*}

    \item
    Použijeme vetu o konštantách a dostávame
    \begin{equation*}
        T \provable \highlighta{((\exists x) D \implies
            D_x[\highlightb{w}])} \implies 
            \highlightc{[B_2 \implies \ldots \implies B_n \implies A]}
    \end{equation*}
    kde $w$ je nová premenná.
    \item
    Teraz môžeme použiť pravidlo zavedenia existenčného kvantifikátora --
    ak je dokázateľné $T \provable A \implies B$ 
    a $w$ nie je voľná v $B$,
    potom je dokázateľné aj $T\provable (\exists w) A \implies B$.
    Čiže
    \begin{equation*}
        T \provable \highlightb{(\exists w)} 
        \highlighta{((\exists x)D \implies D_x[w])}
            \implies 
            \highlightc{[B_2 \implies \ldots \implies B_n \implies A]}
    \end{equation*}

    \item
    Ďalej použijeme prenexnú operáciu $(Qx) (A\implies B) \iff (A\implies
    (Qx)B)$ (za predpokladu, že $x$ nie je voľná v $A$), aby sme $w$
    preniesli dovnútra. Výsledkom je
    \begin{equation*}
        T \provable \highlighta{((\exists x) D \implies 
                \highlightb{(\exists w)}D_x[w])}
            \implies \highlightc{
            [B_2 \implies \ldots \implies B_n \implies A]}
    \end{equation*}

    \item
    Z vety o variantoch ale vieme, že platí (pretože $(\exists w) D_x[w]$ je
    variant $(\exists x) D$) formula
    \begin{equation*}
        T \provable \highlighta{(\exists x) D \implies (\exists w)
        D_x[w]}
    \end{equation*}

    \item
    A teda pomocou pravidla modus ponens získame
    \begin{equation*}
        T \provable \highlightc{
            B_2 \implies B_3 \implies \ldots \implies B_n \implies A}
    \end{equation*}
    \end{itemize}

    Opakovaním postupu ďalších $n-1$ krát dostaneme $T \provable A$.
    Ukázali sme teda, že $T_H$ s jazykom $L(C)$
    je konzervatívne rozšírenie jazyka $L$.
    \\
%%% }}}
\end{dokaz}

\begin{veta}[Lindenbaum]
    Ak $T$ je bezosporná teória s jazykom $L$, potom existuje úplné
    rozšírenie $T'$ teórie $T$ s rovnakým jazykom $L$.
\end{veta}

\begin{dokaz}
%%% {{{
    Nech $\mathscr{S}$ je množina všetkých uzavretých formúl jazyka $L$.
    Ďalej definujeme množinu (podmnožín $\mathscr{S}$)
    $\mathcal{B} = \{ S \mid S \subseteq \mathscr{S}, T \union S
        \mbox{ je bezosporná}\}$.
    Množina $\mathcal{B}$ je čiastočne usporiadaná vzhľadom na
    inklúziu a (ako si neskôr ukážeme) má 
    takzvanú konečnú vlastnosť -- keď zoberieme ľubovoľnú podmnožinu
    $S \subseteq \mathscr{S}$, bude platiť
    \begin{equation*}
        S \in \mathcal{B} \iff \forall \mbox{ konečné } S' \in
        \mathcal{B}: S' \subseteq S
    \end{equation*}
    %
     Potrebujeme ukázať, že operácia inklúzie $\Psi, \Psi \subseteq
     \mathcal{B}\times\mathcal{B}$ je čiastočné usporiadanie, čiže je
    %
    \begin{itemize}
        \item reflexívna
            \begin{align*}
                &\forall S \in \mathcal{B}: (S,S) \in \Psi,
                \quad \mbox{t.j.} \\
                &S \subseteq S
            \end{align*}
        \item antisymetrická
            \begin{align*}
                &(S_1,S_2) \in \Psi \land (S_2,S_1) \in \Psi
                    \then S_1 = S_2, \quad \mbox{t.j.} \\
                &S_1 \subseteq S_2 \land S_2 \subseteq S_1 \then S_1 = S_2
            \end{align*}
        \item tranzitívna (dokážeme analogicky)
    \end{itemize}
    %
    $\mathcal{B}$ je teda čiastočne usporiadaná inklúziou $\Psi$.
    Navyše
    \begin{equation*}
        \emptyset \in \mathcal{B}, \mbox{ lebo } T \union \emptyset = T
    \end{equation*}
    Ak by totiž $\emptyset$ nebola v $\mathcal{B}$, potom by $T$ bola sporná.

    \noindent
    Teraz ukážeme, že množina $\mathcal{B}$ má konečnú vlastnosť, čiže
    platí: Nech $S \in \mathscr{S}$, potom
    \begin{equation*}
            S \in \mathcal{B} \iff \forall \textrm{
        konečnú podmnožinu }S' \subseteq S \textrm{ platí } T \union S' 
            \textrm{ je bezosporná (teda }S' \in \mathcal{B})
    \end{equation*}
   
   \begin{itemize}
       \item[$\Rightarrow:$]
            Nech $S \in \mathcal{B}$. Potom $T \union S$ je bezosporná.
            Ak teda $S' \subseteq S$ a  $S'$ je konečná, teória 
            $T \union S'$ bude tiež bezosporná $\then S' \in \mathcal{B}$

        \item[$\Leftarrow:$]
            Predpokladajme, že pre každú konečnú podmnožinu $S' \subseteq S$
            je $T \union S'$ je bezosporná.
            Chceme ukázať $S' \in \mathcal{B} \then S \in \mathcal{B}$.

            Tvrdenie dokážeme sporom.
            Predpokladajme, že $S \not \in B$.
            Potom $T \union S$ je sporná,
            čiže pre ľubovoľnú dokázateľnú formulu A je dokázateľné
            $\neg(A \implies A)$.

            Nech $A_1, A_2, \dots, A_n$ je dôkaz platnosti 
                $\provable \neg(A \implies A)$.
            Nech $B_1, B_2, \dots, B_m$ sú tie formuly,
            ktoré sa v tom dôkaze vyskytujú a patria do množiny $S$.
            Tvrdíme, že ich počet $m \ge 1$.
            Prečo? Inak by bola priamo $T$ sporná.
            Zoberme teraz ale konečnú množinu $S'=\{B_1, \dots, B_m\}$.
            Zjavne $T \union S'$ je sporná teória.
            To je ale spor s predpokladmi.
    \end{itemize}

    Teraz nachvíľu opustíme dôkaz Lindenbaumovej vety, aby sme
    sformulovali princíp maximality, ktorý sa nám bude hodiť.
    \\
\end{dokaz}

\begin{lema}[Princíp maximality]
    Každá neprázdna podmnožina potenčnej množiny
    $\mathcal{P}(\mathscr{S})$ s konečnou vlastnosťou 
    má maximálny prvok vzhľadom na inklúziu.
\end{lema}

\begin{dokaz}[Pokračovanie dôkazu Lindenbaumovej vety]
    Dostali sme sa do štádia, keď sme ukázali, že $\mathcal{B}$ má
    konečnú vlastnosť. Budeme teda pokračovať tým, že vytvoríme
    rozšírenie pôvodnej teórie nad rovnakým jazykom.

    Nech $S_0$ je maximálny prvok množiny $\mathcal{B}$ vzhľadom na
    inklúziu, podľa princípu maximality existuje.
    Položme rozšírenie $T' = T \union S_0$. Ukážeme, že $T'$ je úplná
    teória, t.j. že pre ľubovoľnú uzavretú formulu $A$ je dokázateľná
    v teórii $T'$ buď $A$ alebo $\neg A$.

    Uvažujme sporom: nech $T'$ nie je úplná teória. 
    Potom existuje uzavretá formula $A$ taká,
    že $T'\not \provable A$ a $T' \not \provable \neg A$.
    Lenže z tohoto je evidentné (keďže $T'$ je bezosporná), že aj
    $T'' = T' \union \{\neg A\}$ je bezosporná teória.\footnote{
        Odvoláme sa na dôsledok vety o dedukcii dokázaný niekedy v
        Úvode do matematickej logiky: ak $A$ je uzavretá,
        potom $T \provable A \iff T \union \{\neg A'\}$ je sporná teória.
    }
    To je ale v spore s tým, že $S_0$ je maximálny prvok $\mathcal{B}$.

    Dosiahli sme zúplnenie teórie. Pre teóriu $T$ sme získali $T'$,
    ktorá je bezosporná a je úplným rozšírením $T$ na rovnakom jazyku.
    \\
%%% }}}    
\end{dokaz}

Zhrňme si, čo sme doteraz dosiahli:
Keď máme teóriu $T$ nad jazykom $L$,
vieme ju rozšíriť na henkinovskú teóriu $T_H$ s jazykom $L(C)$.
V prípade, že $T$ je bezosporná, bude aj $T_H$ bezosporná.
Podľa Lindenbaumovej vety dokážem vytvoriť teóriu $T_H'$ s jazykom
$L(C)$, ktorá je úplná a má model $\mathcal{M}'$.
Našim cieľom je teraz získať model $\mathcal{M}$ pre pôvodnú teóriu.


\begin{definicia}[Redukcia]
    Majme teóriu $T$ nad jazykom $L$ a jej rozšírenie $T',L'$.
    Nech $\mathcal{M}'$ je realizácia jazyka $L'$.
    Redukovaním štruktúry $\mathcal{M}'$ na jazyk $L$
    získame realizáziu teórie $T$ v jazyku $L$.
    Formálne redukciu definujeme nasledovne:
    \begin{itemize}
    \item Univerzum $\mathcal{M}$ bude to isté univerzum ako univerzum
        $\mathcal{M}'$.

    \item $\mathcal{M}$ obsahuje iba také relácie a zobrazenia,
        ktoré realizujú špecálne symboly jazyka $L$ v realizácii
        $\mathcal{M}'$. Teda, ak $f$ je ľubovoľný $n$-ány funkčný
        symbol jazyka $L$ a $f_{\mathcal{M}'}$ je zobrazenie,
        ktoré realizuje $f$ v $\mathcal{M}'$,
        potom zostáva realizáciou $f$ v $\mathcal{M}$.
        Podobne to bude aj s $n$-árnym predikátom $P$.
    \end{itemize}
    
    Budeme hovoriť, že $\mathcal{M}$ vzniklo redukciou $\mathcal{M}'$ 
    na jazyk $L$ a zapisovať 
    $\mathcal{M} = \mathcal{M}' \triangle L$.\footnote{
        Na prednáške bolo miesto $\triangle$ použíté niečo ako $\land$,
        len ľavá nožička bola dlhšia ako pravá.}
    Alebo opačne, $\mathcal{M}'$ je expanzia realizácie $\mathcal{M}$.
\end{definicia}

\begin{poznamka}
    Nech $\mathcal{M}$ je redukcia $\mathcal{M}'$ na jazyk $L$
    a nech $A$ je formula jazyka $L$.
    Potom platí $\mathcal{M} \models A \iff \mathcal{M}' \models A$.
\end{poznamka}
\begin{dokaz}
    Máme teda tvrdenie $\mathcal{M} \models A$, t.j. pre ľubovoľné
    ohodnotenie v relačnej štruktúre $\mathcal{M}$ je formula $A$
    pravdivá. Podobne je to aj s $\mathcal{M}' \models A$.
    Všimnime si, že univerzum je to isté. Nuž ale potom aj ohodnotenia
    premenných musia byť rovnaké. Čo sa týka realizácie
    $\mathcal{M}, \mathcal{M}'$, tak hodnota formuly $A$ závisí
    od realizácie špeciálnych symbolov jazyka $L$. Tie sa ale podľa
    definície realizujú rovnako. Záverom teda je, že pre formulu
    $A$ su realizácie $\mathcal{M}, \mathcal{M'}$ rovnaké a teda platí
    tvrdenie poznámky.
    \\
\end{dokaz}

\begin{veta}
    Nech $T'$ je rozšírenie teórie $T$ s jazykom $L$.
    Ak $\mathcal{M}'$ je model $T'$ a 
    $\mathcal{M} =\mathcal{M}'\triangle L$, tak $\mathcal{M}$ je model $T$.
\end{veta}
\begin{dokaz}
    Nech $A \in T$. Teda, $T \provable A$. Potom (pretože $T'$ je
    rozšírenie $T$) platí $T' \provable A$.
    Čiže z vety o korektnosti dostávame $\mathcal{M}' \models A$. Ale
    $A$ je nad jazykom $L$ a platí $\mathcal{M}= \mathcal{M'}
    \triangle L$. Teda, z predchádzajúcej poznámky vyplýva
    $\mathcal{M} \models A$.
    \\
\end{dokaz}

\noindent
Rozpamätajme sa na náš pôvodný zámer, načo sme sa vlastne zaoberali
rozšíreniami -- bola to práve G\"odelova veta.

\begin{dokaz}[Dokončenie 2. variantu G\"odelovej vety]
    Naším zámerom bolo zostrojiť model pre teóriu, ktorá je bezosporná.
    Postupujme teda nasledovne: K teórii $T$ existuje henkinovské
    rozšírenie $T_H$, ktoré sa dá (konzervatívne) rozšíriť podľa
    Lindenbaumovej vety na úplnú teóriu $T_H'$. O tejto teórii vieme, že
    je bezosporná a teda vieme podľa vety o kanonickej štruktúre
    zostrojiť jej model $\mathcal{M}'$. Nuž a teraz nám stačí redukovať
    $\mathcal{M}'$ na pôvodný jazyk $L$ a dostávame
    $\mathcal{M}= \mathcal{M}' \triangle L$ -- model pôvodnej teórie $T$.
    Naopak, ak k teórii $T$ existoval model, zrejme sa nemôže stať, že by
    bola sporná. Tým sme dokázali 2. variant G\"odelovej vety.
    \\
\end{dokaz}
